Dear Dana:

	John Gill gave me your \F1Data Types as Lattices\F0 and thank you
very much.  I am still pursuing my idea of trying to get a system that
will allow the continuous functions to be axiomatized in first order logic
so that we can combine reasoning about other entities with reasoning about
computable functions.  To this end, about two years ago, I introduced the
idea of extensional forms: an e.f. has free variables in it, but two of them
are equal if they give the same values for all values of the free variables.
The λ becomes just another function that combines a variable and a form to
get another form having one less variable.  The idea seems to work out, but
I haven't pushed it quite far enough to really see.

	Your latest seems promising from my point of view, because it gets
all entities down into a fixed domain, e.g. Pw, and this should make set-theoretic
axiomatization easier.  It occurred to me that for practical purposes it might
be even better to use Ps, where s is the set of LISP S-expressions.  Then the
pairing functions, etc. that you use will be \F1conveniently\F0 computable.

	Enclosed is a printout of a set of axioms for extensional forms, but
I am not sure they are comprehensible without more talk.

						Best Regards,


						John